Nuprl Lemma : isl_wf
12,41
postcript
pdf
A
,
B
:Type,
x
:(
A
+
B
). isl(
x
)
latex
ProofTree
Definitions
isl(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bfalse
wf
,
btrue
wf
origin
A, B:Type, x:(A + B). isl(x) 
A, B:Type, x:(A + B). isl(x)
Tx:A. B(x)